<html>
<head><meta charset="utf-8"><title>chalk #80 smarter subgoal selection · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html">chalk #80 smarter subgoal selection</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="151426366"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151426366" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151426366">(Dec 11 2018 at 06:33)</a>:</h4>
<p>I'm currently looking into this issue; though I haven't really read all of the documentation about how chalk works, i _think_ i have a good enough model of how prolog works, e.g. how it recursively applies rules in order to get to the final goal and backtracks if it went to the wrong direction</p>



<a name="151426443"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151426443" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151426443">(Dec 11 2018 at 06:35)</a>:</h4>
<p>oh, looks like i was basically describing the <code>pursue_strand</code> function's objective!</p>



<a name="151429246"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151429246" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151429246">(Dec 11 2018 at 07:59)</a>:</h4>
<p>i'm thinking of replacing the <code>Vec&lt;Literal&lt;C&gt;&gt;</code> into a <code>BinaryHeap&lt;Literal&lt;C&gt;&gt;</code>, so we can have insertion sort, and we can just pop the first one off the heap</p>



<a name="151430471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151430471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151430471">(Dec 11 2018 at 08:31)</a>:</h4>
<p>hmm, it looks like we need to rearchitect a couple of things too, since <code>SelectedSubgoal</code> stores an index to the <code>subgoal: Vec&lt;Literal&lt;C&gt;&gt;</code> as defined on the X-clause</p>



<a name="151430529"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151430529" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151430529">(Dec 11 2018 at 08:32)</a>:</h4>
<p>and I instead want <code>SelectedSubgoal</code> to store the <code>Literal&lt;C&gt;</code> directly so it manages the ownership</p>



<a name="151432211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151432211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151432211">(Dec 11 2018 at 09:14)</a>:</h4>
<p>ok, that doesn't seem easy, because there seems to be two <code>Context</code> type parameters that I need to be aware of: <code>C</code> and <code>I</code></p>



<a name="151432279"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151432279" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151432279">(Dec 11 2018 at 09:16)</a>:</h4>
<p>I need some way of converting a <code>Literal&lt;C&gt;</code> to a <code>Literal&lt;I&gt;</code>, and vice-versa</p>



<a name="151557212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151557212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151557212">(Dec 12 2018 at 19:34)</a>:</h4>
<p>I'm now abandoning the idea of using a <code>BinaryHeap</code>, because there doesn't seem to be a clean way to interchange the <code>Literal</code> between contexts</p>



<a name="151625224"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151625224" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151625224">(Dec 13 2018 at 17:43)</a>:</h4>
<p>hey <span class="user-mention" data-user-id="116108">@Keith Yeung</span> =)</p>



<a name="151626631"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151626631" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151626631">(Dec 13 2018 at 18:03)</a>:</h4>
<p>Hi</p>



<a name="151722984"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151722984" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151722984">(Dec 13 2018 at 18:46)</a>:</h4>
<p>I instead now iterate over the vec of subgoals and use max() to determine the greatest (least amount of effort) subgoal</p>



<a name="151723042"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151723042" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151723042">(Dec 13 2018 at 18:47)</a>:</h4>
<p>And manually implementing PartialOrd and Ord in a way that makes sense</p>



<a name="151724134"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151724134" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151724134">(Dec 13 2018 at 19:02)</a>:</h4>
<p>I see</p>



<a name="151724152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151724152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151724152">(Dec 13 2018 at 19:02)</a>:</h4>
<p>I am hoping that as we push chalk forward we'll have some "real world" data to help us out here</p>



<a name="151726631"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151726631" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151726631">(Dec 13 2018 at 19:36)</a>:</h4>
<p>so, i have some (probably wrong) heuristics for this:</p>



<a name="151726746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151726746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151726746">(Dec 13 2018 at 19:38)</a>:</h4>
<p>looking at the variants of the <code>Goal</code> enum, I've put <code>CannotProve</code> as the greatest, because there is basically no calculation involved with that goal</p>



<a name="151726992"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151726992" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151726992">(Dec 13 2018 at 19:41)</a>:</h4>
<p>then it's <code>Leaf</code> &gt; <code>Not</code> &gt; <code>Quantified</code> &gt; <code>And</code> &gt; <code>Implies</code></p>



<a name="151727006"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151727006" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151727006">(Dec 13 2018 at 19:41)</a>:</h4>
<p>the way i reached this order is just by counting the number of goals that each variant contains</p>



<a name="151727149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151727149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151727149">(Dec 13 2018 at 19:43)</a>:</h4>
<p>that perhaps may not be the best way, and we might want to reorder <code>And</code>, <code>Not</code> and <code>Quantified</code> to be higher if the operation to separate them into individual <code>Leaf</code> goals is not that expensive</p>



<a name="151727181"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151727181" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151727181">(Dec 13 2018 at 19:43)</a>:</h4>
<p>i do however think there should be an extensive way of ordering the <code>Leaf</code> goals</p>



<a name="151906995"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151906995" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151906995">(Dec 17 2018 at 02:07)</a>:</h4>
<p>opened a PR here <a href="https://github.com/rust-lang-nursery/chalk/pull/193" target="_blank" title="https://github.com/rust-lang-nursery/chalk/pull/193">https://github.com/rust-lang-nursery/chalk/pull/193</a></p>



<a name="151906999"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/151906999" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#151906999">(Dec 17 2018 at 02:07)</a>:</h4>
<p>i'd still like to know if there's a way to benchmark these changes</p>



<a name="152035960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/152035960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#152035960">(Dec 17 2018 at 15:30)</a>:</h4>
<p>cool</p>



<a name="154681585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/154681585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#154681585">(Jan 08 2019 at 22:10)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I believe you mentioned that you want to try a different approach instead?</p>



<a name="155110447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155110447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155110447">(Jan 14 2019 at 19:41)</a>:</h4>
<p><span class="user-mention" data-user-id="116108">@Keith Yeung</span> yeah sorry I didn't get back to you</p>



<a name="155110466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155110466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155110466">(Jan 14 2019 at 19:41)</a>:</h4>
<p>maybe we can chat about this in a bit more depth after the meeting? (e.g., in ~20 minutes, or whenever that comes?) turns out my usual call in that slot got canceled</p>



<a name="155110731"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155110731" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155110731">(Jan 14 2019 at 19:45)</a>:</h4>
<p>sure thing, i should still be available</p>



<a name="155111750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111750">(Jan 14 2019 at 19:59)</a>:</h4>
<p>OK <span class="user-mention" data-user-id="116108">@Keith Yeung</span></p>



<a name="155111755"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111755" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111755">(Jan 14 2019 at 19:59)</a>:</h4>
<p>first off left me review the PR :)</p>



<a name="155111806"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111806" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111806">(Jan 14 2019 at 19:59)</a>:</h4>
<p>Ah, right, so if I recall the PR worked by giving things an order</p>



<a name="155111809"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111809" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111809">(Jan 14 2019 at 19:59)</a>:</h4>
<p>but I'd sort of prefer to make this more customizable</p>



<a name="155111951"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111951" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111951">(Jan 14 2019 at 20:01)</a>:</h4>
<p>one simple option would be to add a callback that can be used <a href="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/logic.rs#L487-L494" target="_blank" title="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/logic.rs#L487-L494">here, when selecting the <code>subgoal_index</code></a></p>



<a name="155111980"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111980" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111980">(Jan 14 2019 at 20:01)</a>:</h4>
<p>something that takes <code>&amp;strand.ex_clause</code> and returns a subgoal index</p>



<a name="155111986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155111986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155111986">(Jan 14 2019 at 20:01)</a>:</h4>
<p>i briefly entertained the idea of giving subgoals a score</p>



<a name="155112053"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112053" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112053">(Jan 14 2019 at 20:02)</a>:</h4>
<p>it seems like it's not necessary for us to be able to independently decide the priority of a subgoal without reference to other subgoals</p>



<a name="155112054"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112054" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112054">(Jan 14 2019 at 20:02)</a>:</h4>
<p>but that scoring system can quickly become really complex</p>



<a name="155112069"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112069" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112069">(Jan 14 2019 at 20:02)</a>:</h4>
<p>we basically just want to know "what to do next"</p>



<a name="155112076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112076">(Jan 14 2019 at 20:02)</a>:</h4>
<p>although in fact I imagine that the implementations often <em>will</em> have a fixed scheme</p>



<a name="155112119"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112119" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112119">(Jan 14 2019 at 20:03)</a>:</h4>
<p>i.e., I think that rustc will deprioritize certain traits and built-in impls and things, particularly when there are unresolved inference variables within</p>



<a name="155112157"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112157" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112157">(Jan 14 2019 at 20:03)</a>:</h4>
<p>hmm... looks like we need a way to peek deeply into the structure of a subgoal</p>



<a name="155112218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112218">(Jan 14 2019 at 20:04)</a>:</h4>
<p>hmm</p>



<a name="155112270"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112270" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112270">(Jan 14 2019 at 20:05)</a>:</h4>
<p>well</p>



<a name="155112285"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112285" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112285">(Jan 14 2019 at 20:05)</a>:</h4>
<p>I think the context will know all the types it needs</p>



<a name="155112297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112297">(Jan 14 2019 at 20:05)</a>:</h4>
<p>that is, we will be giving it a <a href="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/lib.rs#L110-L126" target="_blank" title="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/lib.rs#L110-L126"><code>ExClause</code></a></p>



<a name="155112325"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112325" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112325">(Jan 14 2019 at 20:06)</a>:</h4>
<p>the subgoals therein are a list of <a href="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/lib.rs#L193-L199" target="_blank" title="https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/lib.rs#L193-L199"><code>Literal</code></a></p>



<a name="155112385"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112385" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112385">(Jan 14 2019 at 20:06)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">pub</span><span class="w"> </span><span class="k">enum</span> <span class="nc">Literal</span><span class="o">&lt;</span><span class="n">C</span>: <span class="nc">Context</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// FIXME: pub b/c fold</span>
<span class="w">    </span><span class="n">Positive</span><span class="p">(</span><span class="n">C</span>::<span class="n">GoalInEnvironment</span><span class="p">),</span><span class="w"></span>
<span class="w">    </span><span class="n">Negative</span><span class="p">(</span><span class="n">C</span>::<span class="n">GoalInEnvironment</span><span class="p">),</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>



<a name="155112391"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112391" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112391">(Jan 14 2019 at 20:06)</a>:</h4>
<p>looks like I intended for this stuff to be private, but it ain't</p>



<a name="155112410"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112410" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112410">(Jan 14 2019 at 20:06)</a>:</h4>
<p>anyway, the <code>C::GoalInEnvironment</code> is something that the context knows</p>



<a name="155112463"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112463" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112463">(Jan 14 2019 at 20:07)</a>:</h4>
<p>e.g., <a href="https://github.com/rust-lang/rust/blob/d10680818b2a0aabb76e6a07098e031b31707fcc/src/librustc_traits/chalk_context/mod.rs#L97" target="_blank" title="https://github.com/rust-lang/rust/blob/d10680818b2a0aabb76e6a07098e031b31707fcc/src/librustc_traits/chalk_context/mod.rs#L97">here is the definition in rustc</a></p>



<a name="155112480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112480">(Jan 14 2019 at 20:07)</a>:</h4>
<p>so it ought to be able to figure out which thing it wants to pick</p>



<a name="155112558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112558">(Jan 14 2019 at 20:08)</a>:</h4>
<p>i see, looks like we need some more helper methods/functions in the Context to let us decide what should be evaluated next</p>



<a name="155112584"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112584" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112584">(Jan 14 2019 at 20:09)</a>:</h4>
<p>rather than having the bulk of the logic placed in <code>logic.rs</code></p>



<a name="155112781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112781">(Jan 14 2019 at 20:12)</a>:</h4>
<p>I think .. probably just one method</p>



<a name="155112793"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112793" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112793">(Jan 14 2019 at 20:12)</a>:</h4>
<p>but that is what I had in mind, yeah</p>



<a name="155112808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112808">(Jan 14 2019 at 20:12)</a>:</h4>
<p>I'm trying to decide in which trait it belongs =)</p>



<a name="155112910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112910">(Jan 14 2019 at 20:14)</a>:</h4>
<p>I think either probably the <code>InferenceTable</code> trait</p>



<a name="155112929"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112929" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112929">(Jan 14 2019 at 20:14)</a>:</h4>
<p>or else a new trait analogous to <code>TruncateOps</code> and <code>UnificationOps</code></p>



<a name="155112940"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155112940" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155112940">(Jan 14 2019 at 20:14)</a>:</h4>
<p>i.e., <code>SelectionOps</code></p>



<a name="155113165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155113165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155113165">(Jan 14 2019 at 20:18)</a>:</h4>
<p><span class="user-mention" data-user-id="116108">@Keith Yeung</span> <a href="https://github.com/rust-lang-nursery/chalk/issues/80#issuecomment-454146753" target="_blank" title="https://github.com/rust-lang-nursery/chalk/issues/80#issuecomment-454146753">summarized here</a></p>



<a name="155113171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155113171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155113171">(Jan 14 2019 at 20:18)</a>:</h4>
<p>sound good?</p>



<a name="155113179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155113179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155113179">(Jan 14 2019 at 20:18)</a>:</h4>
<p>Once this lands, next step will be to configure the rustc side :)</p>



<a name="155113202"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/chalk%20%2380%20smarter%20subgoal%20selection/near/155113202" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/chalk.20.2380.20smarter.20subgoal.20selection.html#155113202">(Jan 14 2019 at 20:19)</a>:</h4>
<p>yeah, let's see what i can come up with</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>